Sparsification of Affine Equality Matrix #1625
Conversation
sim642
added
in progress
performance
charlotte-brandt
force-pushed
the
master
branch
from
6b07930 to
f931125
Compare
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
…goblint_lib.ml; Reintroduced Timing.wrap;
File splitting
|
By the way, there are some unresolved comments from @DrMichaelPetter and @michael-schwarz among the long hidden part of this PR. I don't know if there's anything that should still be done w.r.t. those or are they irrelevant by now. |
My remarks will be addressed in a future PR to fine-tune performance, @michael-schwarz issues are concerning the array implementation, which I would also address out of the scope of this course submission, in a cleanup-PR. |
sim642
added
relational
DrMichaelPetter
left a comment
DrMichaelPetter
left a comment
There was a problem hiding this comment.
Ok, one last suggestion: it was probably our fault for not giving you a more precise feedback here: side-effects have a very very different association in the context of the goblint analyzer, and this association is quite dear to us. Let us instead call the property sparse instead of side_effects (which entails inverting the condition), and make the bracketed explanations the actual explanations.
Ideally, also the AffineEqualityDomainSideEffects would rather be the AffineEqualityDenseDomain.
However: With Simmo and me having more or less approved this PR, merging is at the tip of our fingers.
|
The naming regarding the semantics for "side effects" should now be compliant with the goblint standard. I've tried my best to still convey fully the fact that these functions have an effect on the program state. Also the files have been renamed. |
|
Thanks! @CopperCableIsolator: I think you accidentally committed some files in the next to last commit? |
|
Also, I think the conf is not modified yet? |
Co-authored-by: Simmo Saan <[email protected]>
CHANGES: * Add division by zero analysis (goblint/analyzer#1764). * Add bitfield domain (goblint/analyzer#1623). * Add weakly-relational C-2PO pointer analysis (goblint/analyzer#1485). * Add widening delay (goblint/analyzer#1358, goblint/analyzer#1442, goblint/analyzer#1483). * Add narrowing of globals to top-down solver (goblint/analyzer#1636). * Add weak dependencies to top-down solver (goblint/analyzer#1746, goblint/analyzer#1747). * Add YAML ghost witness generation (goblint/analyzer#1394). * Remove GraphML witness generation (goblint/analyzer#1732, goblint/analyzer#1733, goblint/analyzer#1738). * Use C standard option for preprocessing (goblint/analyzer#1807). * Add bash completion for array options (goblint/analyzer#1670, goblint/analyzer#1705, goblint/analyzer#1750). * Make `malloc(0)` semantics configurable (goblint/analyzer#1418, goblint/analyzer#1777). * Update path-sensitive analyses (goblint/analyzer#1785, goblint/analyzer#1791, goblint/analyzer#1792). * Fix evaluation of library function arguments (goblint/analyzer#1758, goblint/analyzer#1761). * Optimize affine equalities analysis using sparse matrices (goblint/analyzer#1459, goblint/analyzer#1625). * Prepare for parallelism (goblint/analyzer#1708, goblint/analyzer#1744, goblint/analyzer#1748, goblint/analyzer#1781, goblint/analyzer#1790).
8 participants
This pull request contributes a sparsification of the
AffineEqualityMatrix(affeq) and is based on the domain of @MartinWehking from this PR.Following restructuring of the modules is introduced:
We added a second
AffineEqualityDomainwhich exploits the sparsity of the affine equality matrices based on this observation by @DrMichaelPetter. ASparseMatrixFunctorandSparseVectorFunctor(as well asArrayMatrixFunctorandArrayVectorFunctor) were added for this purpose and replaced the generalAbstractMatrixandAbstractVector. TheAffineEqualityDomainis now implemented without relying on side effects.The old
AffineEqualityDomainusing arrays was renamed toAffineEqualityDomainSideEffectswhich usesArrayMatrixFunctorandArrayVectorFunctor.No new analysis was added to switch between versions. To switch to the old domain, use
--disable ana.affeq.sparse.The implementation of sparse matrix works as follows:
The sparse matrix is implemented in the
ListMatrixmodule. Itstype tis a list ofsparseVectorsrepresenting the matrix' rows.sparseVectoris implemented as an ordered list of tuples (index, value) for all non-zero entries.Some functions are implemented for zero-preserving functions only. A function is zero-preserving iff it has a fixpoint at zero. These functions are implemented to gain performance when being used on
sparseVectors.This implementation is part of an assignment for the course Automated Bug Hunting and Beyond at TUM in the winter term 2024/25.